| Definitions | Id, P   Q,  x:A. B(x), "$x", Prop,   x. t(x), t  T, 1of(t), ||as||, Top, nth_tl(n;as), l[i],  b, DeclaredType(ds;x),  x:A. B(x), if b t else f fi, {i..j }, i  j < k, A & B, true, s.x, Normal(T), i<j, onceR{$a:ut2, $done:ut2}(i), A, False, Y, false, ij, P & Q, es-realizer(p), hd(l), AB, pre-p-realizable, tl(l), init-p-realizable, @i locl(a) occurs once, e@i.P(e), frame-p-realizable, P  Q, i j, P Q, {T}, P  Q, as @ bs, effect-p-realizable, True,  T, SQType(T), e@i. P(e), x(s), State(ds), ES, @i Precondition for a(v)P State(ds) (v:T), @i x initially v:T, ee'.P(e'), Dec(P), @i only events in L change x : T, (e <loc e'), WellFnd{i}(A;x,y.R(x;y)),  b, isrcv(k), locl(a), isl(x), @i events of kind k change x to f State(ds) (val:T), x initially@i , x when e, (x after e) |
| Lemmas | onceR wf, onceR feasible, once-p wf, implies-es-real, Id wf, event system wf, R-consistent wf, pre-p wf, es-realizer wf, es-real-implies, le wf, fpf-cap-single1, decidable equal bool, decidable ex unit, R-sub-Rlist, fpf-cap-single, es-real wf, eqof eq btrue, normal-ds-single, btrue wf, subtype rel self, R-sub-implies, Reffect wf, Rpre wf, bool wf, decidable wf, fpf-single wf, select member, bool-inhabited, it wf, id-deq wf, unit wf, es-initially wf, atom-free wf, bfalse wf, Rinit wf, init-p wf, es-le-loc, es-kind wf, Knd wf, es-loc wf, change-since-init, assert wf, es-E wf, es-first wf, init-p-implies, locl wf, decidable equal Kind, Rframe wf, frame-p wf, normal-type wf, tl wf, hd wf, length wf1, ge wf, append wf, l member decomp, l member wf, es-locl wf, es-locl-wellfnd, es-vartype wf, es-when wf, es-locl-iff, es-loc-pred, es-axioms, effect-p wf, fpf wf, lnk wf, normal-ds wf, decl-state wf, isrcv wf, ldst wf, decl-type wf, squash wf, true wf, es-after wf, es-pred wf, es-pred-locl, decidable l member, member singleton, eqtt to assert, bool sq |
es.@i locl("a") occurs once